DROPS

Document

DOI: 10.4230/LIPIcs.ITP.2021.12

Homotopy Type Theory in Isabelle

Authors: Joshua Chen

Published in: LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)

Abstract

This paper introduces Isabelle/HoTT, the first development of homotopy type theory in the Isabelle proof assistant. Building on earlier work by Paulson, I use Isabelle’s existing logical framework infrastructure to implement essential automation, such as type checking and term elaboration, that is usually handled on the source code level of dependently typed systems. I also integrate the propositions-as-types paradigm with the declarative Isar proof language, providing an alternative to the tactic-based proofs of Coq and the proof terms of Agda. The infrastructure developed is then used to formalize foundational results from the Homotopy Type Theory book.

Cite as

Joshua Chen. Homotopy Type Theory in Isabelle. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 12:1-12:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{chen:LIPIcs.ITP.2021.12,
  author =	{Chen, Joshua},
  title =	{{Homotopy Type Theory in Isabelle}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{12:1--12:8},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.12},
  URN =		{urn:nbn:de:0030-drops-139072},
  doi =		{10.4230/LIPIcs.ITP.2021.12},
  annote =	{Keywords: Proof assistants, Logical frameworks, Dependent type theory, Homotopy type theory}
}

Search Results

Documents authored by Chen, Joshua

Homotopy Type Theory in Isabelle

Abstract

Cite as

Thanks for your feedback!

Could not send message